/*
 * Copyright 2011, 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree;

import org.w3c.dom.Document;
import org.w3c.dom.Element;

import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePattern;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePatternFactory;
import de.wenzelmf.booleanFunction.util.Tuple;

/**
 * Class representing the auxiliary nodes in the splitting tree.
 * 
 * In contrast to main nodes auxiliary nodes may share successor nodes.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class AuxiliaryNode extends SplittingTreeNode
{
	/*
	 * The <i>l</i> value of the last main node in the tree before this node.
	 */
	protected int l;
	
	/*
	 * The <i>l'</i> value of this node.
	 */
	protected int lPrime;
	
	/**
	 * Construct a new auxiliary node.
	 * 
	 * @param lowerParent The lower parent of the node (referring to the table representation).
	 * @param upperParent The upper parent of the node (referring to the table representation).
	 * @param dnf The DNF associated with this node.
	 * @param occurrencePatterns The occurrence patterns (for all variables that have not been split away yet),
	 * variables are sorted according the relation on occurrence patterns.
	 * @param context Information about the tree this node is used in.
	 * @param l The <i>l</i> value of the last main node in the tree before this node.
	 * @param lPrime The <i>l'</i> value of this node.
	 */
	public AuxiliaryNode(SplittingTreeNode lowerParent,
			SplittingTreeNode upperParent, DNF dnf,
			OccurrencePattern[] occurrencePatterns, TreeContext context, int l, int lPrime)
	{
		super(lowerParent, upperParent, dnf, occurrencePatterns, context);
		this.l = l;
		this.lPrime = lPrime;
	}

	/**
	 * Implements the {@code split} method for auxiliary nodes.
	 * If the upper sibling of this node has already created a lower child this nodes upper child
	 * just uses this node because they coincide.
	 */
	@Override
	public void split(boolean symmetryTest, OccurrencePatternFactory factory, VariableSetting variables,
			ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException
	{
		boolean createBoth = false;
		this.alreadySplit = true;
		if(upperParent != null)
		{
			this.upperChild = upperParent.upperChild.lowerChild;
			this.upperChild.lowerParent = this;
		}
		else
		{
			createBoth = true;
		}
		if(createBoth)
		{
			Tuple<SplitResult, SplitResult> splitResult = splitBoth(factory, variables,
					clauseFactory, dnfFactory);
			SplitResult first = splitResult.getFirst();
			SplitResult second = splitResult.getSecond();
			
			if(createMainNode())
			{
				this.upperChild = new MainNode(this, null, first.dnf, first.patterns, context, first.isFinal);
				this.lowerChild = new MainNode(null, this, second.dnf, second.patterns, context, second.isFinal);
			}
			else
			{
				this.upperChild = new AuxiliaryNode(this, null, first.dnf, first.patterns, context,
						l, lPrime + 1);
				this.lowerChild = new AuxiliaryNode(null, this, second.dnf, second.patterns, context,
						l, lPrime + 1);
			}
		}
		else
		{
			//Tuple<DNF, OccurrencePattern[]> splitResult = splitAway(1, factory, variables,
			//		clauseFactory, dnfFactory);
			SplitResult splitResult = splitAway(1, factory, variables,
							clauseFactory, dnfFactory);
			if(createMainNode())
			{
				this.lowerChild = new MainNode(null, this, splitResult.dnf, splitResult.patterns, context);
			}
			else
			{
				this.lowerChild = new AuxiliaryNode(null, this, splitResult.dnf, splitResult.patterns,
						context, l, lPrime + 1);
			}
		}
	}

	/**
	 * Returns {@code false} because an AuxiliaryNode is never final.
	 * 
	 * @return {@code false}.
	 */
	@Override
	public boolean isFinal()
	{
		return false;
	}
	
	/**
	 * Returns the type of this node, that is "auxiliaryNode".
	 * 
	 * @return "auxiliaryNode".
	 */
	@Override
	public String getType()
	{
		return "auxiliaryNode";
	}
	
	/**
	 * Return {@code true} if this node should create main nodes as successors.
	 * 
	 * @return {@code true} if this node should create main nodes as successors, returns
	 * {@code lPrime == l - 1}.
	 */
	protected boolean createMainNode()
	{
		return lPrime == l - 1;
	}

	/**
	 * Return the <i>l</i> value of the main node before this node.
	 * 
	 * @return The <i>l</i> value of the main node before this node.
	 */
	public int getL()
	{
		return l;
	}

	/**
	 * Return the <i>l'</i> value.
	 * 
	 * @return <i>l'</i>
	 */
	public int getLPrime()
	{
		return lPrime;
	}

	/**
	 * Create a String representation of this node.
	 * 
	 * @return "Auxiliary Node: " + dnf.toString().
	 */
	@Override
	public String toString()
	{
		return "Auxiliary Node: " + dnf;
	}
	
	/**
	 * Return a XML element representing this node as defined in the manual.
	 *  
	 * @param document The root document (use it to create the Element object).
	 * 
	 * @return An element representing this node as defined in the manual.
	 */
	public Element getXMLElement(Document document)
	{
		Element result = super.getXMLElement(document);
		
		result.setAttribute("l", "" + getL());
		result.setAttribute("lPrime", "" + getLPrime());
		
		return result;
	}
}
